\begin{tabbing}
$\forall$\=${\it es}$:ES, $Q_{1}$, $Q_{2}$, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$:Type, ${\it Ia}_{1}$, ${\it Ia}_{2}$:AbsInterface($A$), ${\it Ib}_{1}$,\+
\\[0ex]${\it Ib}_{2}$:AbsInterface($B$), $f$:(E([${\it Ia}_{1}$?${\it Ia}_{2}$])$\rightarrow$$B$).
\-\\[0ex]${\it Ia}_{1}$ $\cap$ ${\it Ia}_{2}$ = 0
\\[0ex]$\Rightarrow$ ${\it Ib}_{1}$ $\cap$ ${\it Ib}_{2}$ = 0
\\[0ex]$\Rightarrow$ Q{-}R{-}glued(${\it es}$; $B$; $f$; ${\it Ia}_{1}$; $Q_{1}$; ${\it Ib}_{1}$; $R$)
\\[0ex]$\Rightarrow$ Q{-}R{-}glued(${\it es}$; $B$; $f$; ${\it Ia}_{2}$; $Q_{2}$; ${\it Ib}_{2}$; $R$)
\\[0ex]$\Rightarrow$ Q{-}R{-}glued(${\it es}$; $B$; $f$; [${\it Ia}_{1}$?${\it Ia}_{2}$]; ($Q_{1}$$\mid$\{${\it Ia}_{1}$\} $\vee$ $Q_{2}$$\mid$\{${\it Ia}_{2}$\}); [${\it Ib}_{1}$?${\it Ib}_{2}$]; $R$)
\end{tabbing}